#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <setjmp.h>
// Apple: #include <malloc.h>
#include <math.h>
#include <string>
#include <vector>
#include <map>
#include <algorithm>
#include <iostream>

using std::string;
using std::vector;
using std::map;
using namespace std;

bool equal_vector(vector<int> *v1, vector<int> *v2) {
  unsigned int n = (unsigned int)v1->size();
  for(unsigned int i=0; i<n; i++) {
    bool flag = true;
    for(unsigned int j=0; j<n; j++)
      if((*v1)[j]!=(*v2)[(i+j)%n]) {
	flag = false;
	break;
      }
    if(flag)
      return true;
  }
  return false;
}

int main(int argc, char* argv[]) {
  
  int N;

  if ( argc != 2 ) {
    cout << "Usage: card-gen <N> " << endl;
    cout << "Where N is the number of children, > 2" << endl;
    exit(1);
  }
  else {
    N = atoi(argv[1]);
  }
  
  cout << "-- The protocol for the card game" << endl <<
    "-- This file is automatically generated for " << N <<
    " cards (N is even number)" << endl << endl;

  cout << "Agent Environment" << endl <<
    "  Obsvars:" << endl <<
    "    a: 0.." << (N/2-1) << ";" << endl << 
    "    b: 0.." << (N/2-1) << ";" << endl << 
    "  end Obsvars" << endl << endl <<
    "  Vars:" << endl;
  for(int i=1; i<=2; i++)
    for(int j=1; j<N/2; j++)
      cout << "    c"<< i << j << ": 1.." << N << ";" << endl;
  cout <<"  end Vars" << endl << endl <<
    "  RedStates:" << endl <<
    "  end RedStates" << endl << endl <<
    "  Actions = { watch, null };" << endl <<
    "  Protocol:" << endl <<
    "    a+b<" << (N/2-1) <<": {watch};" << endl <<
    "    Other: {null};" << endl <<
    "  end Protocol" << endl << endl <<
    "  Evolution:" << endl;
  for(int j=1; j<(N/2); j++) {
    cout << "    a=a+1 if c1" << j << ">c2" << j << " and " <<
      "Player1.Action=playcard" << j << " and " <<
      "Player2.Action=playcard" << j << ";" << endl;
    cout << "    b=b+1 if c1" << j << "<c2" << j << " and " <<
      "Player1.Action=playcard" << j << " and " <<
      "Player2.Action=playcard" << j << ";" << endl;
  }
    
  cout << "  end Evolution" << endl << 
    "end Agent" << endl << endl;

  
  for (int i=0; i < 2; i++) {
    cout << "Agent Player" << i+1 << endl;
    cout << "  Vars:" << endl;
    cout << "    n: {a1";
    for(int j=2; j<=N/2; j++)
      cout << ", a" << j;
    cout << "};" << endl;
    for(int j=1; j<N/2; j++)
      cout << "    c" << j << ": 1.." << N << ";" << endl;
    cout << "  end Vars" << endl;
    cout << "  RedStates:" << endl;
    cout << "  end RedStates" << endl;
    cout << "  Actions = {";
    for(int j=1; j<N/2; j++)
      cout << "playcard" << j << ", ";
    cout << "null};" << endl;
    cout << "  Protocol:" << endl;
    for(int j=1; j<N/2; j++)
      cout << "    n=a" << j << ": {playcard" << j << "};" << endl;
    cout << "    n=a" << (N/2) << ": {null};" << endl;
    cout << "  end Protocol" << endl;
  	
    cout << "  Evolution:" << endl;
    for(int j=1; j<(N/2); j++)
      cout << "    n=a" << (j+1) << " if n=a" << j << ";" << endl;
    cout << "  end Evolution" << endl;

    cout << "end Agent" << endl << endl;
  }


  cout << "Evaluation" << endl;
  for ( int i=1; i <= 2; i++ ) {
    cout << "  allred" << i << " if Player1.c1>" << (N/2);
    for(int j=2; j<N/2; j++) 
      cout << " and Player" << i <<".c" << j << ">" << (N/2);
    cout << ";" << endl;
  }
  cout << "  win1 if Environment.a>Environment.b;" << endl;
  cout << "  win2 if Environment.b>Environment.a;" << endl;
 
  cout << "end Evaluation" << endl << endl;
  
  
  cout << "InitStates" << endl;
  cout << "  Player1.n=a1 and Player2.n=a1 and Environment.a=0 and Environment.b=0 and (" << endl;

  for(int i=1; i<N/2; i++) {
    cout << "    (";
    for(int j=1; j<=N; j++) {
      if(j>1)
	cout << "     ";
      cout << "(Player1.c" << i << "=" << j << " and Environment.c1" 
	   << i << "=" << j << " and !(";
      for(int k=i+1; k<N/2; k++)
	cout << "Player1.c" << k << "=" << j << " or ";
      for(int k=1; k<N/2; k++) {
	cout << "Player2.c" << k << "=" << j;
	if(k<N/2-1) 
	  cout << " or ";
      }
      if(j<N)
	cout << ")) or " << endl;
      else
	cout << "))";
    }
    cout << ") and" << endl;
  }

  for(int i=1; i<N/2; i++) {
    cout << "    (";
    for(int j=1; j<=N; j++) {
      if(j>1)
	cout << "     ";
      cout << "(Player2.c" << i << "=" << j << " and Environment.c2" 
	   << i << "=" << j << "";
      if(i+1<N/2) {
	cout << " and !(";
	for(int k=i+1; k<N/2; k++) {
	  cout << "Player2.c" << k << "=" << j;
	  if(k<N/2-1)
	    cout << " or ";
	}
	cout << ")";
      }
      if(j<N)
	cout << ") or " << endl;
      else
	cout << ")";
    }
    if(i<N/2-1)
      cout << ") and" << endl;
    else
      cout << ")";
  }
  cout << ");" << endl;
  

  cout << "end InitStates" << endl << endl;

  cout << "Groups" << endl;
  cout << "end Groups" << endl << endl;

  cout << "Fairness" << endl;
  cout << "end Fairness" << endl << endl;

  cout << "Formulae"<< endl;
  
  cout << "  AG(allred1 -> K(Player1, AF win1));" << endl;
  //cout << "  AG(allred2 -> K(Player2, AF win2));" << endl;


  cout << "end Formulae" << endl;

}

